\begin{tabbing} (\=(UnivCD THENA Auto) \+ \\[0ex]CollapseTHEN (((AutoBoolCase $y$) \\[0ex]CollapseTHEN ((((( \-\\[0ex]RWO "eqtt\_to\_assert" 0) \\[0ex]C\=ollapseTHENA (Auto$\cdot$))$\cdot$) \+ \\[0ex]CollapseTHEN ((((( \-\\[0ex]RWO "eqff\_to\_assert" 0) \\[0ex]C\=ollapseTHENA (Auto$\cdot$))$\cdot$) \+ \\[0ex]CollapseTHEN ((((( \-\\[0ex]RW assert\_pushdownC 0) \\[0ex]C\=ollapseTHENA (Auto$\cdot$))$\cdot$) \+ \\[0ex]CollapseTHEN (Auto$\cdot$))$\cdot$))$\cdot$))$\cdot$))$\cdot$))$\cdot$ \- \end{tabbing}